|
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov. It is also sometimes called the realizability interpretation, because of the connection with the realizability theory of Stephen Kleene. == The interpretation == The interpretation states exactly what is intended to be a proof of a given formula. This is specified by induction on the structure of that formula: *A proof of is a pair <''a'', ''b''> where ''a'' is a proof of ''P'' and ''b'' is a proof of ''Q''. *A proof of is a pair <''a'', ''b''> where ''a'' is 0 and ''b'' is a proof of ''P'', or ''a'' is 1 and ''b'' is a proof of ''Q''. *A proof of is a function ''f'' that converts a proof of ''P'' into a proof of ''Q''. *A proof of is a pair <''a'', ''b''> where ''a'' is an element of ''S'', and ''b'' is a proof of ''φ(a)''. *A proof of is a function ''f'' that converts an element ''a'' of ''S'' into a proof of ''φ(a)''. *The formula is defined as , so a proof of it is a function ''f'' that converts a proof of ''P'' into a proof of . *There is no proof of (the absurdity). The interpretation of a primitive proposition is supposed to be known from context. In the context of arithmetic, a proof of the formula ''s''=''t'' is a computation reducing the two terms to the same numeral. Kolmogorov followed the same lines but phrased his interpretation in terms of problems and solutions. To assert a formula is to claim to know a solution to the problem represented by that formula. For instance is the problem of reducing ''Q'' to ''P''; to solve it requires a method to solve problem ''Q'' given a solution to problem ''P''. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Brouwer–Heyting–Kolmogorov interpretation」の詳細全文を読む スポンサード リンク
|